Nuprl Lemma : mkfpf_wf
11,40
postcript
pdf
A
:Type,
a
:(
A
List),
b
:({
a@0
:
A
| (
a@0
a
)}
Top). mkfpf(
a
;
b
)
a
:
A
fp
Top
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
a
:
A
fp
B
(
a
)
,
mkfpf(
a
;
b
)
,
Lemmas
l
member
wf
,
top
wf
origin
A:Type, a:(A List), b:({a@0:A| (a@0 
a)} 
Top). mkfpf(a;b) a:A fp Top A:Type, a:(A List), b:({a@0:A| (a@0 a)} Top). mkfpf(a;b) a:A fp Top x:A. B(x) T B(a)